\begin{tabbing}
(\=D ({-}1)$\cdot$) \+
\\[0ex]CollapseTHEN ((Using [`n',$m$] (BLemma `can{-}apply{-}fun{-}exp`) ) 
\\[0ex]CollapseTHEN (
\-\\[0ex]Auto$\cdot$)$\cdot$)$\cdot$
\end{tabbing}